r:RngSig, P:(|r|). IsPrimeIdeal(r;P)   

latex

Up	rings 1
Definitions of Statement	IsPrimeIdeal(R;P)
Definitions	P  Q, x f y, P  Q, P & Q, IsPrimeIdeal(R;P), t  T, , x:A. B(x)
Lemmas	rng sig wf, rng times wf, rng car wf, rng one wf, not wf